ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id, e1,e2:{e:es-E(es)| 
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id, e1,e2:{loc(e) = i} ,
L1,L2:(event-info(ds;da) List).
((L1 = []))
 ((L2 = []))
 (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (es-hist{i:l}(es;e1;e2) = append(L1; L2)  (event-info(ds;da) List))
 e(e1,e2].(es-hist{i:l}(es;e1;es-pred(es; e)) = L1)  (es-hist{i:l}(es;e;e2) = L2) 

latex

Definitions

b, P  Q, False, A, x:A. B(x), t  T, loc(e), Id, es-hist{i:l}(es;e1;e2), event-info(ds;da), P  Q, e(e1,e2].P(e), x. t(x), fpf(A; a.B(a)), Knd, event_system{i:l}, es-E(es), prop{i:l}, top, id-deq, fpf-cap(f; eq; x; z), es-vartype(es; i; x), es-kind(es; e), Kind-deq, es-valtype(es; e), append(as; bs), [e, e'], guard(T), sq_type(T), ||as||, es-info(es;e), map(f; as), subtype(S; T), ge(i; j), es-pred(es; e), A  B, , es-le(es; e; e'), P  Q, P  Q, A c B, es-locl(es; e; e'), t.1, x:A. B(x), (x  l), P  Q

Lemmas

map append sq, es-interval wf, general-append-cancellation, es-info wf, member-es-interval, list-subtype, subtype rel list, l member wf, map wf, es-interval-partition, es-locl wf, es-le wf, es-pred wf, es-le-loc, es-locl-iff, es-interval-non-zero, es-subinterval, pos length, length-map, length-append, length wf1, Id sq, es-interval wf2, append wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, not wf, event-info wf, es-E wf, es-loc wf, event system wf, Knd wf, fpf wf, Id wf, es-hist wf, es-loc-pred